Inference at * 1 1 3 
Iof proof for Lemma decidable atom equal:

.....subterm..... T:t3:n

1. a : Atom
2. b : Atom
3. a = b
  (inl Ax )  ((a = b)  ((a = b))) 

latex

 by MemberEqCD 

latex

 1: .....subterm..... T:t1:n

 1:   Ax  (a = b)
 2: .....eq aux..... NILNIL

 2:   ((a = b))  Type
 .

Definitions	P  Q, t  T
Lemmas	not wf